


\section{Introduction}

\emph{Session types} 
%have been intensively studied as 
offer a powerful type-theoretic foundation 
%formal models 
for the analysis of
%represent one of the most studied foundations for analyzing 
complex scenarios of structured communications, as frequently found in service-oriented systems.  
They abstract communication protocols as basic interaction patterns, which
%. As a simple example, 
%the session type
%$?(\mathsf{tweet}).!(\mathsf{ok}). \epsilon$
%can be assigned to a server that first \emph{receives} a value of type $\mathsf{tweet}$, then \emph{sends} a value of type $\mathsf{ok}$, 
%and \emph{finishes}. 
%These basic patterns
are then statically checked against specifications
in some core programming calculus---typ\-i\-cal\-ly, a variant of the $\pi$-calculus.
%This way, e.g., the session type
%$?(\mathsf{tweet}).!(\mathsf{ok}). \epsilon$
%can be assigned to a server that first \emph{receives} a value of type $\mathsf{tweet}$, then \emph{sends} a value of type $\mathsf{ok}$, 
%and \emph{finishes}. 
%Correctness is enforced through \emph{duality}: 
%our server will interact correctly only with clients with type $!(\mathsf{tweet}).?(\mathsf{ok}). \epsilon$.
Introduced in~\cite{DBLP:conf/concur/Honda93,DBLP:conf/esop/HondaVK98}, 
session type theories 
have been extended in many directions---see~\cite{DBLP:conf/wsfm/Dezani-Ciancaglinid09} for a survey.
%so as to cover, e.g., %forms of 
%higher-order~\cite{DBLP:conf/tlca/MostrousY07} and 
%multiparty~\cite{DBLP:conf/popl/HondaYC08} %, and asynchronous~\cite{DBLP:conf/forte/KouzapasYH11} 
%communication. % (See~\cite{DBLP:conf/wsfm/Dezani-Ciancaglinid09} for a survey.)
Their practical relevance %of session types 
is witnessed by, e.g., 
%functional~\cite{DBLP:conf/haskell/PucellaT08} and object-oriented~\cite{DBLP:conf/coordination/NgYPHK11} implementations, and by 
 their application in the verification of parallel systems~\cite{DBLP:conf/tools/NgYH12}.


%However, and in 
In spite of these developments, 
we find that existing ses\-sion-typed
%programming 
calculi do not explicitly support 
for reasoning about \emph{runtime adaptation}. % such as runtime adaptation and dynamic reconfiguration.
%}\footnote{Name passing can be considered a form of dynamic reconfiguration}
While channel mobility (\emph{delegation}~\cite{DBLP:journals/entcs/YoshidaV07}) 
as supported by such calculi
is often useful to model forms of
dynamic reconfiguration, more general forms of adaptation/evolvability 
are not expressible or are hard to reason about.
%Adaptation and evolvability are increasingly relevant issues nowadays, 
Runtime adaptation is an increasingly relevant issue nowadays, 
as distributed systems and applications are  being deployed in
open, highly dynamic infrastructures, such as cloud computing platforms.
In such settings,  
runtime adaptation %and dynamic reconfiguration  
appears as a key feature to
%are central capabilities to 
ensure continued system operation,
reduce costs, and achieve
business agility. %\todo{maybe a sentence on sessions here}

We thus observe a rather unfortunate discrepancy between 
(i)~the evolvability capabilities of modern distributed systems in practice, and 
(ii)~the forms of interaction available in the calculi 
upon which session types disciplines are defined.
 %(essentially, variants of the $\pi$-calculus)


In this paper, we propose an approach towards overcoming this discrepancy.
We %extend an existing 
introduce a
session types discipline 
for a language
equipped
with 
mechanisms for runtime adaptation.
Rather than developing yet another session types discipline \emph{from scratch}, we have deliberately 
preferred to build upon two existing lines of work. 
Our proposal %approach types discipline 
 results from combining 
the %main insights of the 
framework of 
\emph{adaptable processes}, which we have developed together with Bravetti and Zavattaro in~\cite{BGPZFMOODS}, with
the main insights %principles %underlying the discipline 
of the session type system
put forward by Garralda et al.~\cite{DBLP:conf/ppdp/GarraldaCD06}. 
%On the one hand, based on a limited form of higher-order communication, 
While %the framework in~\cite{BGPZFMOODS} 
adaptable processes
%While the latter work
represent an attempt for enhancing process calculi specifications with evolvability mechanisms, 
%the former . On the other hand, 
the work in~\cite{DBLP:conf/ppdp/GarraldaCD06} 
develops a %theory for \emph{safe}\footnote{\small{In~\cite{DBLP:conf/ppdp/GarraldaCD06}, \emph{safety} refers to the proper interaction of mobility steps and communication, and so it differs from the usual notion of type safety. To avoid confusion, here we use the adjective \emph{consistent}.}} 
session types theory for the Boxed Ambient calculus~\cite{DBLP:journals/toplas/BugliesiCC04}.
Despite these seemingly distant origins, %we believe that 
our framework %presented here %, we believe,
combines the most interesting ideas of both approaches into a simple yet expressive model 
of structured communications with explicit mechanisms for runtime adaptation.

We briefly describe our approach and results. 
%We consider a
Our  process language includes
%equipped with 
a set of standard $\pi$-calculus constructs, extended 
with the \emph{located processes} and the \emph{update processes} introduced in~\cite{BGPZFMOODS}.
Given a location $l$, a process $P$, and a context $Q(\mathsf{X})$ 
(i.e. a process with free occurrences of variable $\mathsf{X}$), these processes are noted $l[P]$ and $l\{Q(\mathsf{X})\}$, resp. 
They may interact so as to evolve into process 
$Q\subst{P}{\mathsf{X}}$, which represents the \emph{update} of  process $P$ at $l$ with a reconfiguration routine 
(or built-in adaptation mechanism)
embodied by $Q(\mathsf{X})$. Locations can be nested and are transparent:
within $l[P]$, process $P$ can evolve autonomously, with the potential of interacting with some neighboring 
update process $l\{Q(\mathsf{X})\}$, as just described. 
Hence, %This way, 
%in the adaptable processes %intuitive description may be useful to realize how in the framework of~\cite{BGPZFMOODS} 
%framework evolvability corresponds to a form of (higher-order) process mobility. 
in our language communicating behavior coexists with update actions. 
This raises the need for disciplining both forms of interaction, 
respecting session types descriptions but also enforcing evolvability requirements. 
To this end, by observing that %exploiting the fact that 
update corresponds to a form of (higher-order) process mobility, 
%This observation is the key to understand the relationship 
%we establish a relationship with the session types 
we draw inspiration from the session types 
in~\cite{DBLP:conf/ppdp/GarraldaCD06}.
Indeed, 
%by injecting in the syntax some constructs supporting static analysis,
such a type discipline 
%a main contribution of
%in~\cite{DBLP:conf/ppdp/GarraldaCD06} %is the technical machinery that 
ensures that
session communications within Ambient hierarchies %are \emph{safe}, i.e., they 
do not get interrupted by Ambient mobility steps. 
We call this property \emph{session consistency}.

While both Ambients and adaptable processes rely on nested located processes,
Ambient mobility and evolvability steps are conceptually very different.
In fact, %is a major difference:
%The main difference between the two is that, while 
Ambient mobility is only defined in a parent-child style, whereas
%in~\cite{BGPZFMOODS}
%synchronizations between 
located processes and update actions 
 may interact independently of their relative position in the hierarchy induced by location nesting.
This way, integrating our calculus for adaptable processes %of~\cite{BGPZFMOODS} 
with the session types discipline in~\cite{DBLP:conf/ppdp/GarraldaCD06}
roughly amounts to: 
(1)~generalizing the operational semantics of~\cite{DBLP:conf/ppdp/GarraldaCD06}
so as to account for adaptation in \emph{arbitrary process hierarchies}; 
(2)~endowing the evolvability constructs %of~\cite{BGPZFMOODS} 
with suitable \emph{annotations}, describing the session behavior embodied in located and update processes; and 
(3)~extending the typing judgments of~\cite{DBLP:conf/ppdp/GarraldaCD06}, so as to be able to reason about 
\emph{process interfaces}.
%``offered behavior'', 
%as described by the annotations described in (2). 
Ultimately, this last step is what realizes a form of \emph{typeful adaptation}, which contrasts with the untyped adaptation in~\cite{BGPZFMOODS}.  Well-typed processes 
in our framework
satisfy basic correctness guarantees (formalized as a Subject Reduction result), 
which entails consistency for session-typed processes %that
%including the \emph{session safety} of~\cite{DBLP:conf/ppdp/GarraldaCD06} (here called \emph{consistency}), adapted to the case of processes which 
%may be updated at runtime.
with runtime adaptation mechanisms.

This work is an initial %yet concrete 
step towards a theory of interaction
in which processes---endowed with behavioral disciplines expressed as types---may dynamically evolve at runtime. 
We have focused on session consistency---a basic 
approach to discipline
%consequence of considering 
the interplay of evolvability steps 
%(represented by the update of located processes) 
and communication behavior. % (represented by session interactions).
Issues such as deadlock-freedom, resource usage, and trustworthiness %, and reliability 
are also important---we plan to look into these in the future. 
Nevertheless, we believe that a major contribution of our paper %is novel, as it 
is to address issues which, to our knowledge, have not yet  been explored in the realm of 
%formal models for the specification and verification of distributed systems, such.
session-typed %interacting 
processes. \\

\noindent\textbf{Organization.~}
%The rest of the paper is structured as follows:
Sect.~\ref{sec:syn} presents our process language, and Sect.~\ref{s:types} defines our session type system.
In Sect.~\ref{sec:res} we state our main results (subject reduction and session consistency); an illustrative example is given in Sect.~\ref{sec:exam}.
We discuss interface compatibility for update actions in Sect.\ref{sec:int}.
Finally, Sect.~\ref{sec:rw} discusses related work and Sect.~\ref{sec:conc} collects some concluding remarks.
%An extended version of this paper, with proofs and additional examples, is available online.\footnote{{\scriptsize \url{http://www.jorgeaperez.net/publications/sac13ext.pdf}}}
%and discussions is~\cite{dGP-long}.

%In the light of the above description, we think that the main merit of this paper  lies in its originality and relevance:
%we show how the integration of evolvability concerns into an existing session types framework is both important and feasible.
%While the overall technical contribution could be considered minor (in the sense that we adapt/extend known theoretical frameworks),
%we believe that our paper is novel, as it 
%addresses issues which, to the best of our knowledge, have yet not been explored in the realm of formal models for the specification and 
%verification of distributed systems.


%An important research strand on formal models for distributed computing is based upon
%\emph{process calculi}. These small formalisms for concurrency turn out to be particularly 
%adequate for specifying complex behavioral patterns of interacting systems. 
%More importantly, as they support powerful reasoning techniques, 
%%such as type systems and logics, 
%process calculi provide a firm basis for rigorously developing novel
%programming languages and verification tools. 
%Within such reasoning techniques, static analysis techniques based on type systems have received much attention.
%They have proved useful to enforce important correctness properties (e.g., protocol conformance, resource usage, deadlock-freedom)
%on system specifications by disciplining the interaction of concurrent processes. 
%
%It is interesting to reflect on the way in which typed disciplines for 
%structured communications have evolved.
%There have been many recent developments, aimed at capturing different phenomena (asynchronous communication, multiparty protocols);
%as a result, the degree of specialization of the typing disciplines, 
%rather than on the interaction patterns present on the underlying languages.
%Indeed, most (if not all) of the emerging typing systems for disciplining concurrent processes  
%build upon essentially the \emph{same} underlying formalism, namely variants of the $\pi$-calculus.
%This trend seems to suggest that, at least for specifying 
%structured communications,
% the $\pi$-calculus (and its dialects) are the undisputable languages for concurrency.
%In other words, 
%
%that essentially everything has been said about the linguistic foundations of concurrent and interactive computing. 
%
%In this paper, we wish to challenge the latter perception. 
%We examine the well-known typing discipline of session types by putting it in the context 
%of a concurrent language that enhances the $\pi$-calculus with a simple form of dynamic adaptation.
%Dynamic adaptation refers to the possibility of replacing or discarding a system component at runtime; it is 
%thus a form of interaction that appears difficult to represent via the name passing feature of the $\pi$-calculus.
%We feel that the inherent dynamicity of interacting services begs for more
%sophisticated theories of interacting processes in which issues such as adaptation, runtime reconfiguration 
%are explicitly addressed.
%To carry out our development, rather than proposing a new formalism for concurrent processes, 
%we build on ideas and insights from previous works. 
%More precisely, we combine the classic model of session types with previous developments by Garralda et al 
%---on session types for the Ambient calculus---and by Bravetti et al---on concurrent adaptable processes.
